($\lambda$$E$,$T$,$x$,$z$. tree\_leaf($x$)) $\in$ $E$,$T$:Type$\rightarrow$$E$$\rightarrow\downarrow$True$\rightarrow$tree\_con($E$;$T$)